T, A:Type, P:(AT), k:Knd, i, r, x:Id.
Normal(T)
 Normal(A)
 ((r = x))
 ((isrcv(k))  (i = destination(lnk(k))))
 es.recognizer-p(es;T;A;P;k;i;r;x) 

latex

Definitions

P  Q, P  Q, {T}, SQType(T), A c B, e@i. P(e), P & Q, , tt, if b then t else f fi , Top, x. t(x), x(s), t  T, recognizer-p(es;T;A;P;k;i;r;x), P  Q, x:A. B(x), (state when e), ES, recognizer(es;i;ds;x;k;T;test), State(ds)

Lemmas

es-first wf, es-dtype wf, es-when-first-discrete, fpf-cap-single1, es-state-subtype-iff, Knd sq, Id sq, es-valtype-kindtype, es-E wf, es-loc wf, es-kind wf, bool wf, Knd wf, normal-type wf, not wf, lnk wf, ldst wf, isrcv wf, recognizer wf, es-real-monotonicity, normal-ds-single, fpf-single-dom, top wf, fpf-dom wf, assert wf, not functionality wrt iff, subtype rel self, eqof eq btrue, id-deq wf, fpf-cap-single, Id wf, fpf-single wf, recognizer-realizable